;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: equality-elimination2.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2005.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

;;; based on constraint equality elimination (CEE) transformation in
;;; Bachmair, Ganzinger, and Voronkov
;;; "Elimination of Equality via Transformation with Ordering Constraints"
;;; CADE-15
;;;
;;; Notes:
;;; * returns results as single clauses
;;;   constraint literals can be extracted for inclusion in row-constraints
;;; * no specialization for constant that is minimal in ordering
;;;   if e is minimal, (ordering-gt e x) is unsatisfiable and (ordering-ge e x) implies x=e
;;; * no specialization for skolems
;;; * (not (= x y)) literals are eliminated by resolution with reflexivity
;;;   instead of being replaced by an equality constraint
;;; * adding constraints is done as separate transformation at the end
;;;   because new equality literals are systematically constrained
;;;   (= a b) : (ordering-gt a b), (not (= a b)) : (ordering-ge a b)
;;;   thus propagating constraints throughout transformation process is unnecessary
;;; * when flattening, replace terms by variable everywhere they appear
;;;   (= a (g a)) -> (or (not (= a x)) (= x (g x))) instead of
;;;   (= a (g a)) -> (or (not (= a x)) (= a (g x)))

(declare-snark-option equality-elimination-new-equality-symbol-name '=ee :never-print)
(declare-snark-option equality-elimination-maximum-number-of-positive-equality-literals 10 :never-print)
(declare-snark-option trace-equality-elimination nil :never-print)

(defun equality-eliminate-wff (wff)
  ;; for use only if wff is a clause or conjunction of clauses
  (if (or (eq true wff) (eq false wff))
      wff
      (let ((clauses nil) clauses-last)
        (prog->
          (map-conjuncts wff ->* clause)
          (equality-eliminate-clause clause ->* clause)
          (collect clause clauses))
        (conjoin* clauses))))

(defun equality-eliminate-clause (cc clause)
  (prog->
    (atoms-in-clause2 clause -> atoms-and-polarities)
    (equality-eliminate-clause2 atoms-and-polarities ->* atoms-and-polarities)
    (atoms-to-clause2 atoms-and-polarities -> clause)
    (funcall cc clause)))

(defun equality-eliminate-clause2 (cc atoms-and-polarities)
  (prog->
    (equality-elimination-maximum-number-of-positive-equality-literals? ->nonnil maxcount)
    (quote 0 -> count)
    (dolist atoms-and-polarities ->* x)
    (first x -> atom)
    (second x -> polarity)
    (when (and (eq :pos polarity) (compound-p atom) (eq *=* (head atom)) (< maxcount (incf count)))
      (warn "Equality elimination is ignoring clause ~S that has more than ~D positive equality literals." atoms-and-polarities maxcount)
      (funcall cc atoms-and-polarities)
      (return-from equality-eliminate-clause2)))
  (let ((step1-clauses nil)
        (step2-clauses nil)
        (step3-clauses nil)
        (step4-clauses nil)
        (step5-clauses nil))
    (prog->
      (ee-new-equality-symbol -> new=)
      (ee-ordering-gt-symbol -> gt)
      (ee-ordering-ge-symbol -> ge)
      (ee-flatten-clause atoms-and-polarities ->* atoms-and-polarities)
      (when (trace-equality-elimination?) (push atoms-and-polarities step1-clauses))
      (ee-reflex-clause atoms-and-polarities ->* atoms-and-polarities)
      (when (trace-equality-elimination?) (push atoms-and-polarities step2-clauses))
      (ee-symm-clause atoms-and-polarities new= ->* atoms-and-polarities)
      (when (trace-equality-elimination?) (push atoms-and-polarities step3-clauses))
      (ee-trans-clause atoms-and-polarities new= ->* atoms-and-polarities)
      (when (trace-equality-elimination?) (push atoms-and-polarities step4-clauses))
      (ee-constrain-clause atoms-and-polarities new= gt ge ->* atoms-and-polarities)
      (when (trace-equality-elimination?) (push atoms-and-polarities step5-clauses))
      (funcall cc atoms-and-polarities))
    (when (trace-equality-elimination?)
      (format t "~2%Equality elimination input:") (print atoms-and-polarities)
      (format t "~2%After M transformation:") (mapc 'print (reverse step1-clauses))
      (format t "~2%After R transformation:") (mapc 'print (reverse step2-clauses))
      (format t "~2%After S transformation:") (mapc 'print (reverse step3-clauses))
      (format t "~2%After T transformation:") (mapc 'print (reverse step4-clauses))
      (format t "~2%After adding constraints:") (mapc 'print (reverse step5-clauses)))
    nil))

(defun ee-reflex-clause (cc atoms-and-polarities &optional new-atoms-and-polarities subst)
  ;; use reflexivity to eliminate negative equality literals when both arguments are variables
  ;; unify the variables instead of adding an equality constraint
  ;; what if variables are sorted?
  (cond
   ((null atoms-and-polarities)
    (funcall cc (instantiate (reverse new-atoms-and-polarities) subst)))
   (t
    (prog->
      (first atoms-and-polarities -> x)
      (first x -> atom)
      (second x -> polarity)
      (and (compound-p atom) (eq *=* (head atom)) (args atom) -> args)
      (cond
       ((and args (eq :neg polarity) (variable-p (first args)) (variable-p (second args)))
        (unify (first args) (second args) subst ->* subst)
        (ee-reflex-clause cc (rest atoms-and-polarities) new-atoms-and-polarities subst))
       (t
        (ee-reflex-clause cc (rest atoms-and-polarities) (cons x new-atoms-and-polarities) subst)))))))

(defun ee-symm-clause (cc atoms-and-polarities &optional (new= (ee-new-equality-symbol)))
  ;; use symmetry to reverse arguments of positive literals
  ;; (or (= a b) (= c d)) -> (and (or (= a b) (= c d))
  ;;                              (or (= b a) (= c d))
  ;;                              (or (= a b) (= d c))
  ;;                              (or (= b a) (= d c)))
  ;; also replace (not (= x a)) by (not (= a x))
  (cond
   ((null atoms-and-polarities)
    (funcall cc atoms-and-polarities))
   (t
    (prog->
      (first atoms-and-polarities -> x)
      (first x -> atom)
      (second x -> polarity)
      (and (compound-p atom) (eq *=* (head atom)) (args atom) -> args)
      (ee-symm-clause (rest atoms-and-polarities) new= ->* l)
      (cond
       (args
        (ecase polarity
          (:pos
           (funcall cc (cons (list (make-compound new= (first args) (second args)) :pos) l))
           (funcall cc (cons (list (make-compound new= (second args) (first args)) :pos) l)))
          (:neg
           (funcall cc (cons (list (if (variable-p (first args)) (make-compound new= (second args) (first args)) (make-compound new= (first args) (second args))) :neg) l)))))
       (t
        (funcall cc (cons x l))))))))

(defun ee-trans-clause (cc atoms-and-polarities &optional (new= (ee-new-equality-symbol)))
  ;; use transitivity to turn positive equality literals into implications
  ;; (= a b) -> (or (not (= a ?x)) (= ?x b))
  (let ((new-atoms-and-polarities nil) new-atoms-and-polarities-last
;;      (gt (ee-ordering-gt-symbol))
;;      (ge (ee-ordering-ge-symbol))
        )
    (prog->
      (dolist atoms-and-polarities ->* x)
      (first x -> atom)
      (second x -> polarity)
      (and (compound-p atom) (eq new= (head atom)) (args atom) -> args)
      (cond
       (args
        (let ((arg1 (first args))
              (arg2 (second args)))
          (cond
           ((not (variable-p arg2))
            (let ((var (make-variable)))			;what sort?
              (collect (list (make-compound new= arg2 var) :neg) new-atoms-and-polarities)
              (collect (list (make-compound new= arg1 var) polarity) new-atoms-and-polarities)
;;            (collect (list (make-compound ge arg2 var) :neg) new-atoms-and-polarities)
;;            (collect (list (make-compound (if (eq :pos polarity) gt ge) arg1 var) :neg) new-atoms-and-polarities)
              ))
           (t
            (collect (list (make-compound new= arg1 arg2) polarity) new-atoms-and-polarities)
;;          (collect (list (make-compound (if (eq :pos polarity) gt ge) arg1 arg2) :neg) new-atoms-and-polarities)
            ))))
         (t
          (collect x new-atoms-and-polarities))))
    (funcall cc new-atoms-and-polarities)))

(defun ee-constrain-clause (cc atoms-and-polarities &optional (new= (ee-new-equality-symbol)) (gt (ee-ordering-gt-symbol)) (ge (ee-ordering-ge-symbol)))
  ;; in CEE, (= a b) literals are always constrained by (ordering-gt a b) and
  ;;   (not (= a b)) literals are always constrained by (ordering-ge a b)
  ;; so, we add constraint literals in a separate transformation, instead of during the transitivity transformation
  (cond
   ((eq :unconstrained (use-equality-elimination?))
    (funcall cc atoms-and-polarities))
   (t
    (let ((constraint-atoms-and-polarities nil) constraint-atoms-and-polarities-last)
      (prog->
        (dolist atoms-and-polarities ->* x)
        (first x -> atom)
        (second x -> polarity)
        (and (compound-p atom) (eq new= (head atom)) (args atom) ->nonnil args)
        (first args -> arg1)
        (second args -> arg2)
        (collect (list (make-compound (if (eq :pos polarity) gt ge) arg1 arg2) :neg) constraint-atoms-and-polarities))
      (funcall cc (append atoms-and-polarities constraint-atoms-and-polarities))))))

(defun ee-flatten-clause (cc atoms-and-polarities)
  (loop
    (let ((v (ee-find-term-to-flatten2 atoms-and-polarities)))
      (cond
       ((eq none v)
        (funcall cc atoms-and-polarities)
        (return))
       (t
        (let ((var (make-variable)))			;what sort?
          (setf atoms-and-polarities
                (cons (list (make-compound *=* v var) :neg)
                      (mapcar (lambda (x) (list (substitute var v (first x)) (second x))) atoms-and-polarities)))))))))

(defun ee-find-term-to-flatten2 (atoms-and-polarities)
  ;; find a nonvariable term with an occurrence other than as an equality argument
  (dolist (x atoms-and-polarities none)
    (let* ((atom (first x))
           (v (ee-find-term-to-flatten1 atom)))
      (unless (eq none v)
        (return v)))))

(defun ee-find-term-to-flatten1 (atom)
  (cond
   ((not (compound-p atom))
    none)
   ((eq *=* (head atom))
    (first-nonvariable-subterm (args atom)))
   (t
    (first-nonvariable-term (args atom)))))

(defun ee-new-equality-symbol ()
  (declare-relation (equality-elimination-new-equality-symbol-name?) 2 :rewrite-code '(equality-rewriter) :satisfy-code '(reflexivity-satisfier)))

(defun ee-ordering-gt-symbol ()
  (declare-relation 'ordering> 2 :constraint-theory 'ordering))

(defun ee-ordering-ge-symbol ()
  (declare-relation 'ordering>= 2 :constraint-theory 'ordering))

(defun ee-convert (&optional (name "GRP001-1"))
  (declare (special *tptp-input-directory*))
  (initialize)
  (use-equality-elimination :unconstrained)
  (equality-elimination-new-equality-symbol-name 'eeequal)
  (use-assertion-analysis nil)
  (use-simplification-by-equalities nil)
  (use-simplification-by-units nil)
  (use-subsumption nil)
  (print-options-when-starting nil)
  (print-summary-when-finished nil)
  (print-rows-when-derived nil)
  (agenda-length-limit nil)
  (agenda-length-before-simplification-limit nil)
  (mapc #'eval (list* `(assertion (,(equality-elimination-new-equality-symbol-name?) ?x ?x) :reason assertion :name reflexivity)
                      (read-assertion-file (make-pathname :name (string name) :type "tptp" :directory *tptp-input-directory*) :format :tptp)))
  (closure)
  (let ((name (concatenate 'string (string name) "+eq_elim"))
        (type "tptp"))
    (with-open-file (*standard-output* (make-pathname :name name :type type :directory *tptp-input-directory*) :direction :output :if-exists :supersede)
      (format t "%------------------------------------------------------------------------------~%")
      (format t "% ~A" name)
      (print-rows :format :tptp)
      (format t "~%%------------------------------------------------------------------------------~%")))
  nil)

;;; equality-elimination2.lisp EOF
